-----------------------------
MODULE capability_wrapper
-----------------------------

EXTENDS capability_system, TLC

(*
 * ZENrs Capability Wrapper 形式化模型
 *
 * 此模块形式化描述了 safe_services/src/lib.rs 中的 Capability 结构体行为
 * 验证其安全属性，包括获取/释放的正确性、所有权模型和资源管理
 *)

(* 定义进程类型 *)
Process == [id: ProcessId, capabilities: Set(CapabilityId)]

(* 系统状态定义 *)
VARIABLES 
    \* 当前活动的进程集合
    processes,
    
    \* exokernel能力表 (CapabilityId -> OwnerId)
    exokernel_cap_table,
    
    \* Capability包装器状态表 (WrapperId -> [id: CapabilityId, acquired: Bool])
    capability_wrappers,
    
    \* 当前活动的包装器ID集合
    live_wrappers

(* 常量定义 *)
InitProcessId == 1
MemoryCapabilityId == 100
CPUCapabilityId == 101

(* 初始状态 *)
Init ==
    /\ processes = {[id |-> InitProcessId, capabilities |-> {MemoryCapabilityId, CPUCapabilityId}]}
    /\ exokernel_cap_table = [
        MemoryCapabilityId |-> InitProcessId,
        CPUCapabilityId |-> InitProcessId
    ]
    /\ capability_wrappers = [
        1 |-> [id |-> MemoryCapabilityId, acquired |-> FALSE],
        2 |-> [id |-> CPUCapabilityId, acquired |-> FALSE]
    ]
    /\ live_wrappers = {1, 2}

(* 能力获取操作 *)
AcquireCapability(wrapperId) ==
    /\ wrapperId \in live_wrappers
    /\ ~capability_wrappers[wrapperId].acquired
    /\ LET capId = capability_wrappers[wrapperId].id
        owner = exokernel_cap_table[capId]
        currentProcess = CHOOSE p \in processes: p.id = InitProcessId
    IN 
        /\ owner = currentProcess.id
        /\ capability_wrappers' = [capability_wrappers EXCEPT ![wrapperId].acquired = TRUE]
        /\ UNCHANGED <<processes, exokernel_cap_table, live_wrappers>>

(* 能力释放操作 *)
ReleaseCapability(wrapperId) ==
    /\ wrapperId \in live_wrappers
    /\ capability_wrappers[wrapperId].acquired
    /\ capability_wrappers' = [capability_wrappers EXCEPT ![wrapperId].acquired = FALSE]
    /\ UNCHANGED <<processes, exokernel_cap_table, live_wrappers>>

(* 包装器析构操作 *)
DestroyWrapper(wrapperId) ==
    /\ wrapperId \in live_wrappers
    /\ LET 
        capId = capability_wrappers[wrapperId].id
        isAcquired = capability_wrappers[wrapperId].acquired
    IN 
        /\ (isAcquired => exokernel_cap_table' = [exokernel_cap_table EXCEPT ![capId] = InitProcessId])
        /\ (isAcquired => capability_wrappers' = [capability_wrappers EXCEPT ![wrapperId].acquired = FALSE])
        /\ (isAcquired => UNCHANGED live_wrappers)
        /\ (~isAcquired => capability_wrappers' = capability_wrappers)
        /\ (~isAcquired => live_wrappers' = live_wrappers \ {wrapperId})
        /\ UNCHANGED processes

(* 创建新包装器 *)
CreateWrapper(capId) ==
    /\ capId \in DOMAIN exokernel_cap_table
    /\ LET 
        newWrapperId = IF live_wrappers = {} THEN 1 ELSE Max(live_wrappers) + 1
        currentProcess = CHOOSE p \in processes: p.id = InitProcessId
    IN 
        /\ exokernel_cap_table[capId] = currentProcess.id
        /\ capability_wrappers' = capability_wrappers @@ [newWrapperId |-> [id |-> capId, acquired |-> FALSE]]
        /\ live_wrappers' = live_wrappers \union {newWrapperId}
        /\ UNCHANGED processes

(* 下一个状态 *)
Next ==
    \E wrapperId \in live_wrappers:
        AcquireCapability(wrapperId) \/
        ReleaseCapability(wrapperId) \/
        DestroyWrapper(wrapperId)
    \/
    \E capId \in DOMAIN exokernel_cap_table:
        CreateWrapper(capId)

(* 安全属性定义 *)

(* 能力获取后状态一致性：获取的能力在exokernel表中应归当前进程所有 *)
CapabilityAcquireConsistency == 
    \A wrapperId \in live_wrappers:
        capability_wrappers[wrapperId].acquired => 
        exokernel_cap_table[capability_wrappers[wrapperId].id] = InitProcessId

(* 能力释放后不可访问：释放的能力在包装器中标记为未获取 *)
CapabilityReleaseSafety == 
    \A wrapperId \in live_wrappers:
        ~capability_wrappers[wrapperId].acquired => 
        TRUE  (* 在我们的模型中，释放仅更改包装器状态，不影响exokernel表 *)

(* Drop时自动释放：析构的包装器确保能力被正确处理 *)
CapabilityDropSafety == 
    \A capId \in DOMAIN exokernel_cap_table:
        \A wrapperId \in (DOMAIN capability_wrappers) \ live_wrappers:
            capability_wrappers[wrapperId].id = capId => 
            ~capability_wrappers[wrapperId].acquired

(* 资源所有权一致性：每个能力在exokernel表中只能属于一个进程 *)
ResourceOwnershipConsistency == 
    \A capId \in DOMAIN exokernel_cap_table:
        exokernel_cap_table[capId] = InitProcessId

(* 活性属性：任何未获取的能力最终都可以被获取 *)
CapabilityLiveness == 
    \A wrapperId \in live_wrappers:
        ~capability_wrappers[wrapperId].acquired => 
        <>capability_wrappers[wrapperId].acquired

(* 验证配置 *)

(* 模型检查的不变式 *)
Spec == Init /\ [][Next]_<<processes, exokernel_cap_table, capability_wrappers, live_wrappers>>

(* 要验证的不变式 *)
Inv == 
    CapabilityAcquireConsistency /\
    CapabilityReleaseSafety /\
    CapabilityDropSafety /\
    ResourceOwnershipConsistency

(* TLC配置 *)

(* 限制状态空间大小 *)
CONSTANTS MaxProcesses = 1, MaxCapabilities = 2, MaxWrappers = 5

(* 模型检查 *)
Check == TLC!Spec \/\ TLC!Inv

(*
运行此模型：
1. 使用TLA+工具box打开此文件
2. 配置TLC模型检查器，设置不变式为Inv
3. 运行模型检查

预期结果：
- 所有不变式应成立
- 没有违反安全属性的状态
*)